; <lemma>
;  <title>ch915_sort_other.3</title>
;  <origin>ch915_sort_other | sort_m1 | thm4/THM</origin>
(benchmark ch915_sort_other_3
;  <theories>
;    <theory name="linear_order_int"/>
;    <theory name="basic_set"/>
;  </theories>
  :logic AUFLIA
;  <typenv>
;    <variable name="n" type="INTEGER"/>
;    <variable name="a" type="INTEGER"/>
;    <variable name="b" type="INTEGER"/>
;  </typenv>
  :extrafuns ((n Int)
	       (a Int)
	       (b Int))
  :extramacros (
		 (in (lambda (?x 't) (?p ('t boolean)) . (?p ?x)))
		 (range (lambda (?i1 Int) (?i2 Int) .
			  (lambda (?i Int) .
			    (and (<= ?i1 ?i) (<= ?i ?i2)))))
		 (couple (lambda (?x 't) (?y 't) . 
			   (lambda (?z 't) . (or (= ?z ?x) (= ?z ?y)))))
		 (setminus
		   (lambda (?p1 ('t boolean)) (?q1 ('t boolean)) .
		     (lambda (?x 't) . (and (?p1 ?x) (not (?q1 ?x))))))
		 (ismax
		   (lambda (?m Int) (?pi (Int boolean))  .
		     (and (?pi ?m)
		       (forall (?i1 Int) . (implies (?pi ?i1) (<= ?i1 ?m))))))
		 (union
		   (lambda (?p1 ('t boolean)) (?q1 ('t boolean)) .
		     (lambda (?x 't) . (or (?p1 ?x) (?q1 ?x)))))
		 )
; <hypothesis needed="true">a : 1 .. n</hypothesis>
  :assumption (in a (range 1 n))
; <hypothesis needed="true">b : 1 .. n</hypothesis>
  :assumption (in b (range 1 n))
; <goal>(1 .. n - {a,b})\/{a,b} = 1 .. n</goal>
  :formula
  (not
    (= (union 
	 (setminus (range 1 n) (couple a b))
	 (couple a b))
      (range 1 n))
    )
)
; </lemma>

